<!DOCTYPE html>
<html lang="zh">
    <head>
        <meta charset="utf-8">
        <meta http-equiv="X-UA-Compatible" content="IE=edge,chrome=1">
        <title>软件安全安全相关文献阅读笔记 | ChenDong Zhu&#39;s Blog</title><meta name="viewport" content="width=device-width, initial-scale=1.0">
<meta name="robots" content="noodp" />
<meta name="Description" content="软件安全的论文阅读笔记"><link rel="prev" href="/2021/09/algebra/" /><link rel="next" href="/2021/10/%E6%9C%BA%E5%99%A8%E5%AD%A6%E4%B9%A0/" /><link rel="canonical" href="/2021/09/%E8%BD%AF%E4%BB%B6%E5%AE%89%E5%85%A8/" />
<link rel="shortcut icon" type="image/x-icon" href="/favicon.ico" />
<link rel="apple-touch-icon" sizes="180x180" href="/apple-touch-icon.png">
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
<link rel="manifest" href="/site.webmanifest">
<link rel="mask-icon" href="/safari-pinned-tab.svg" color="#5bbad5">
<meta name="msapplication-TileColor" content="#da532c">
<meta name="theme-color" content="#ffffff"><meta property="og:title" content="软件安全安全相关文献阅读笔记" />
<meta property="og:description" content="软件安全的论文阅读笔记" />
<meta property="og:type" content="article" />
<meta property="og:url" content="/2021/09/%E8%BD%AF%E4%BB%B6%E5%AE%89%E5%85%A8/" /><meta property="article:section" content="posts" />
<meta property="article:published_time" content="2021-09-27T09:00:00+08:00" />
<meta property="article:modified_time" content="2020-09-27T09:00:00+08:00" />

<meta name="twitter:card" content="summary"/>
<meta name="twitter:title" content="软件安全安全相关文献阅读笔记"/>
<meta name="twitter:description" content="软件安全的论文阅读笔记"/>
<script type="application/ld+json">
    {
        "@context": "http://schema.org",
        "@type": "BlogPosting",
        "headline": "软件安全安全相关文献阅读笔记",
        "mainEntityOfPage": {
            "@type": "WebPage",
            "@id": "\/2021\/09\/%E8%BD%AF%E4%BB%B6%E5%AE%89%E5%85%A8\/"
        },"image": {
                "@type": "ImageObject",
                "url": "\/cover.png",
                "width":  800 ,
                "height":  600 
            },"genre": "posts","keywords": "信息安全, 区块链","wordcount":  869 ,
        "url": "\/2021\/09\/%E8%BD%AF%E4%BB%B6%E5%AE%89%E5%85%A8\/","datePublished": "2021-09-27T09:00:00\u002b08:00","dateModified": "2020-09-27T09:00:00\u002b08:00","license": "This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.","publisher": {
                "@type": "Organization",
                "name": "xxxx",
                "logo": {
                "@type": "ImageObject",
                "url": "\/logo.png",
                "width":  127 ,
                "height":  40 
                }
            },"description": "软件安全的论文阅读笔记"
    }
    </script><link rel="stylesheet" href="/css/style.min.css"><link rel="stylesheet" href="/css/lib/fontawesome-free/all.min.css"><link rel="stylesheet" href="/css/lib/animate/animate.min.css"></head>
    <body><script>
            window.isDark = (window.localStorage && window.localStorage.getItem('theme')) === 'dark';
            window.isDark && document.body.classList.add('dark-theme');
        </script><div class="wrapper"><nav class="navbar">
    <div class="navbar-container">
        <div class="navbar-header animated bounceIn">
            <a href="/">ChenDong Zhu&#39;s Blog</a>
        </div>
        <div class="navbar-menu"><a class="menu-item" href="/posts" title="">文章</a><a class="menu-item" href="/tags" title="">标签</a><a class="menu-item" href="/categories" title="">分类</a><a class="menu-item" href="/about" title="">关于</a><a class="menu-item" href="https://hugo-loveit-en.netlify.com" title="English"><i class="fas fa-language fa-fw"></i></a><a href="javascript:void(0);" class="theme-switch"><i class="fas fa-adjust fa-rotate-180 fa-fw" title="切换主题"></i></a>
        </div>
    </div>
</nav><nav class="navbar-mobile">
    <div class="navbar-container">
        <div class="navbar-header">
            <div class="navbar-header-title animated bounceIn">
                <a href="/">ChenDong Zhu&#39;s Blog</a>
            </div>
            <div class="menu-toggle" id="menu-toggle">
                <span></span><span></span><span></span>
            </div>
        </div>
        <div class="navbar-menu" id="mobile-menu"><a class="menu-item" href="/posts" title="">文章</a><a class="menu-item" href="/tags" title="">标签</a><a class="menu-item" href="/categories" title="">分类</a><a class="menu-item" href="/about" title="">关于</a><a class="menu-item" href="https://hugo-loveit-en.netlify.com" title="English"></a><a href="javascript:void(0);" class="theme-switch"><i class="fas fa-adjust fa-rotate-180 fa-fw" title="切换主题"></i></a>
        </div>
    </div>
</nav><main class="main">
                <div class="container"><article class="page"><h1 class="post-title animated flipInX">软件安全安全相关文献阅读笔记</h1><div class="post-meta">
            <div class="post-meta-main"><a class="author" href="/" rel="author" target="_blank">
                    <i class="fas fa-user-circle fa-fw"></i>ChenDong Zhu
                </a>&nbsp;<span class="post-category">收录于&nbsp;<i class="far fa-folder fa-fw"></i><a href="/categories/%E5%AD%A6%E4%B9%A0/">学习</a>&nbsp;</span></div>
            <div class="post-meta-other"><i class="far fa-calendar-alt fa-fw"></i><time datetime=2021-09-27>2021-09-27</time>&nbsp;
                <i class="fas fa-pencil-alt fa-fw"></i>约 869 字&nbsp;
                <i class="far fa-clock fa-fw"></i>预计阅读 2 分钟&nbsp;</div>
        </div><div class="post-toc" id="post-toc">
                <h2 class="post-toc-title">目录</h2>
                <div class="post-toc-content"><nav id="TableOfContents">
  <ul>
    <li><a href="#1-symbolic-execution-for-software-testing-three-decades-later">1 Symbolic Execution for Software Testing: Three Decades Later</a>
      <ul>
        <li><a href="#创新点内容">创新点/内容</a></li>
        <li><a href="#文章内容">文章内容</a>
          <ul>
            <li><a href="#符号执行概念">符号执行概念</a></li>
            <li><a href="#符号执行碰到的问题">符号执行碰到的问题</a></li>
            <li><a href="#非线性或者调用api">非线性、或者调用api</a></li>
            <li><a href="#现代符号执行技术">现代符号执行技术</a></li>
            <li><a href="#imprecision和completeness">Imprecision和completeness</a></li>
            <li><a href="#加速约束求解的方法">加速约束求解的方法</a></li>
            <li><a href="#约束求解的问题">约束求解的问题</a></li>
            <li><a href="#内存模型">内存模型</a></li>
            <li><a href="#处理并发问题">处理并发问题</a></li>
          </ul>
        </li>
      </ul>
    </li>
  </ul>
</nav></div>
            </div>
            <div class="post-toc-mobile" id="post-toc-mobile">
                <details>
                    <summary>
                        <div class="post-toc-title">
                            <span>目录</span>
                            <span><i class="details icon fas fa-angle-down"></i></span>
                        </div>
                    </summary>
                    <div class="post-toc-content"><nav id="TableOfContentsMobile">
  <ul>
    <li><a href="#1-symbolic-execution-for-software-testing-three-decades-later">1 Symbolic Execution for Software Testing: Three Decades Later</a>
      <ul>
        <li><a href="#创新点内容">创新点/内容</a></li>
        <li><a href="#文章内容">文章内容</a>
          <ul>
            <li><a href="#符号执行概念">符号执行概念</a></li>
            <li><a href="#符号执行碰到的问题">符号执行碰到的问题</a></li>
            <li><a href="#非线性或者调用api">非线性、或者调用api</a></li>
            <li><a href="#现代符号执行技术">现代符号执行技术</a></li>
            <li><a href="#imprecision和completeness">Imprecision和completeness</a></li>
            <li><a href="#加速约束求解的方法">加速约束求解的方法</a></li>
            <li><a href="#约束求解的问题">约束求解的问题</a></li>
            <li><a href="#内存模型">内存模型</a></li>
            <li><a href="#处理并发问题">处理并发问题</a></li>
          </ul>
        </li>
      </ul>
    </li>
  </ul>
</nav></div>
                </details>
            </div><div class="post-content"><a class="post-dummy-target" id="1-symbolic-execution-for-software-testing-three-decades-later"></a><h2>1 Symbolic Execution for Software Testing: Three Decades Later</h2>
<p>作者: Cristian Cadar, Koushik Sen</p>
<p>文献链接:<a href="http://www.cs.umd.edu/class/fall2017/cmsc818O/papers/symbolic-execution.pdf" target="_blank">Symbolic Execution for Software Testing: Three Decades Later</a></p>
<a class="post-dummy-target" id="创新点内容"></a><h3>创新点/内容</h3>
<ul>
<li>综述，总览经典、现代符号执行技术的发展，以及其挑战与可能的解决方案，并展示相关工具</li>
</ul>
<a class="post-dummy-target" id="文章内容"></a><h3>文章内容</h3>
<a class="post-dummy-target" id="符号执行概念"></a><h4>符号执行概念</h4>
<p>程序中每个<code>if</code>语句都是一个约束，如果约束为真则程序执行<code>then</code>语句块，如果约束为假则进入<code>else</code>语句块，对于指定一条程序执行path，将该path上所有约束合在一起，用约束求解器，求解出每个变量具体的值</p>
<a class="post-dummy-target" id="符号执行碰到的问题"></a><h4>符号执行碰到的问题</h4>
<ul>
<li>循环
<ul>
<li>循环代表可能会有无限的<code>if</code></li>
</ul>
</li>
<li>路径爆炸</li>
<li>约束难以求解（对于非线性的函数）</li>
<li>内存模型</li>
</ul>
<a class="post-dummy-target" id="非线性或者调用api"></a><h4>非线性、或者调用api</h4>
<div class="highlight"><div class="chroma">
<table class="lntable"><tr><td class="lntd">
<pre tabindex="0" class="chroma"><code><span class="lnt"> 1
</span><span class="lnt"> 2
</span><span class="lnt"> 3
</span><span class="lnt"> 4
</span><span class="lnt"> 5
</span><span class="lnt"> 6
</span><span class="lnt"> 7
</span><span class="lnt"> 8
</span><span class="lnt"> 9
</span><span class="lnt">10
</span><span class="lnt">11
</span><span class="lnt">12
</span></code></pre></td>
<td class="lntd">
<pre tabindex="0" class="chroma"><code class="language-c" data-lang="c"><span class="kt">int</span> <span class="nf">twice</span> <span class="p">(</span><span class="kt">int</span> <span class="n">v</span><span class="p">){</span>
	<span class="k">return</span> <span class="p">(</span><span class="n">v</span><span class="o">*</span><span class="n">v</span><span class="p">)</span> <span class="o">%</span> <span class="mi">50</span><span class="p">;</span>
<span class="p">}</span>

<span class="kt">void</span> <span class="nf">testme</span><span class="p">(</span><span class="kt">int</span> <span class="n">x</span><span class="p">,</span> <span class="kt">int</span> <span class="n">y</span><span class="p">){</span>
    <span class="n">z</span> <span class="o">=</span> <span class="n">twice</span><span class="p">(</span><span class="n">y</span><span class="p">);</span>
    <span class="k">if</span><span class="p">(</span><span class="n">z</span> <span class="o">==</span> <span class="n">x</span><span class="p">)</span> <span class="p">{</span>
        <span class="k">if</span><span class="p">(</span><span class="n">x</span> <span class="o">&gt;</span> <span class="n">y</span> <span class="o">+</span> <span class="mi">10</span><span class="p">){</span>
            <span class="n">ERROR</span><span class="p">;</span>
        <span class="p">}</span>
    <span class="p">}</span>
<span class="p">}</span>
</code></pre></td></tr></table>
</div>
</div><p>对于上面的<code>z == x</code>展开后就是<code>y*y%50 == x</code>，这对于约束求解器来说是非线性的，较难求解，同时如果<code>twice</code>是一个第三方库的api，没有源码，那也无法求解</p>
<a class="post-dummy-target" id="现代符号执行技术"></a><h4>现代符号执行技术</h4>
<ul>
<li>Concolic Testing：先用具体的值，具体的值执行后会显示一条path，这条path就可以不用符号执行了（大概是这个意思吧），或者这条path在经过小小的符号执行就可以变成另一条path</li>
<li>Execution-Generated Testing(EGT)，如果约束涉及到的都是具体的值，那么就采用concrete execution，如果有一个值是Symbol那么就采用符号执行</li>
</ul>
<p>以上其实都可以成为动态符号执行技术</p>
<a class="post-dummy-target" id="imprecision和completeness"></a><h4>Imprecision和completeness</h4>
<p>在不准确和完备之间需要做一个trade between，可以采用启发式方法</p>
<a class="post-dummy-target" id="加速约束求解的方法"></a><h4>加速约束求解的方法</h4>
<ul>
<li>Irrelevant constraint elimination，因为不是所有的if约束都相关的，可能第一个约束和变量<code>x</code>有关，第二个约束和变量<code>y</code>有关，只考虑相关的约束进行求解</li>
<li>增量求解，因为很多程序的执行path都是有“公共祖先”的，即存在部分约束是相同的，可以存储一些约束的解进入cache,后面可以查看这个约束是否求解过了，如果求解过了就直接调用cache中的答案</li>
</ul>
<a class="post-dummy-target" id="约束求解的问题"></a><h4>约束求解的问题</h4>
<ul>
<li>处理指针重赋值</li>
<li>处理数组索引</li>
</ul>
<a class="post-dummy-target" id="内存模型"></a><h4>内存模型</h4>
<p>算术溢出等问题将导致符号执行失去path</p>
<a class="post-dummy-target" id="处理并发问题"></a><h4>处理并发问题</h4>
<p>并发问题的测试比较困难，如分布式系统，GPGPU程序等</p>
</div><div class="post-footer" id="post-footer">
    <div class="post-info">
        <div class="post-info-line">
            <div class="post-info-mod">
                <span>本文于 2020-09-27 更新</span>
            </div>
            <div class="post-info-license"></div>
        </div>
        <div class="post-info-line">
            <div class="post-info-md"></div>
            <div class="post-info-share"><span><a href="//twitter.com/share?url=%2f2021%2f09%2f%25E8%25BD%25AF%25E4%25BB%25B6%25E5%25AE%2589%25E5%2585%25A8%2f&amp;text=%e8%bd%af%e4%bb%b6%e5%ae%89%e5%85%a8%e5%ae%89%e5%85%a8%e7%9b%b8%e5%85%b3%e6%96%87%e7%8c%ae%e9%98%85%e8%af%bb%e7%ac%94%e8%ae%b0&amp;via=" target="_blank" title="分享到 Twitter">
            <i class="fab fa-twitter fa-fw"></i>
        </a><a href="//www.facebook.com/sharer/sharer.php?u=%2f2021%2f09%2f%25E8%25BD%25AF%25E4%25BB%25B6%25E5%25AE%2589%25E5%2585%25A8%2f" target="_blank" title="分享到 Facebook">
            <i class="fab fa-facebook-square fa-fw"></i>
        </a><a href="//reddit.com/submit?url=%2f2021%2f09%2f%25E8%25BD%25AF%25E4%25BB%25B6%25E5%25AE%2589%25E5%2585%25A8%2f&amp;title=%e8%bd%af%e4%bb%b6%e5%ae%89%e5%85%a8%e5%ae%89%e5%85%a8%e7%9b%b8%e5%85%b3%e6%96%87%e7%8c%ae%e9%98%85%e8%af%bb%e7%ac%94%e8%ae%b0" target="_blank" title="分享到 Reddit">
            <i class="fab fa-reddit fa-fw"></i>
        </a><a href="//service.weibo.com/share/share.php?url=%2f2021%2f09%2f%25E8%25BD%25AF%25E4%25BB%25B6%25E5%25AE%2589%25E5%2585%25A8%2f&amp;appkey=&amp;title=%e8%bd%af%e4%bb%b6%e5%ae%89%e5%85%a8%e5%ae%89%e5%85%a8%e7%9b%b8%e5%85%b3%e6%96%87%e7%8c%ae%e9%98%85%e8%af%bb%e7%ac%94%e8%ae%b0" target="_blank" title="分享到 Weibo">
            <i class="fab fa-weibo fa-fw"></i>
        </a></span></div>
        </div>
    </div>

    <div class="post-info-more">
        <section><span class="tag">
                        <a href="/tags/%E4%BF%A1%E6%81%AF%E5%AE%89%E5%85%A8/"><i class="fas fa-tag fa-fw"></i>&nbsp;信息安全</a>&nbsp;
                    </span><span class="tag">
                        <a href="/tags/%E5%8C%BA%E5%9D%97%E9%93%BE/"><i class="fas fa-tag fa-fw"></i>&nbsp;区块链</a>&nbsp;
                    </span></section>
        <section>
            <span><a href="javascript:window.history.back();">返回</a></span>&nbsp;|&nbsp;<span><a href="/">主页</a></span>
        </section>
    </div>

    <div class="post-nav"><a href="/2021/09/algebra/" class="prev" rel="prev" title="代数学习笔记"><i class="fas fa-angle-left fa-fw"></i>代数学习笔记</a>
            <a href="/2021/10/%E6%9C%BA%E5%99%A8%E5%AD%A6%E4%B9%A0/" class="next" rel="next" title="机器学习">机器学习<i class="fas fa-angle-right fa-fw"></i></a></div>
</div><div class="post-comment"></div>
    </article></div>
            </main><footer class="footer">
    <div class="copyright"><div class="copyright-line">由 <a href="https://gohugo.io/" target="_blank" rel="external nofollow noopener noreffer">Hugo</a> 强力驱动 | 主题 - <a href="https://github.com/dillonzq/LoveIt" target="_blank" rel="external nofollow noopener noreffer">LoveIt<i class="far fa-heart fa-fw"></i></a>
        </div>

        <div class="copyright-line"><i class="far fa-copyright fa-fw"></i><span itemprop="copyrightYear">2020 - 2021</span><span class="author" itemprop="copyrightHolder">&nbsp;<a href="/" target="_blank">ChenDong Zhu</a></span>&nbsp;|&nbsp;<span class="license"><a rel="license external nofollow noopener noreffer" href="https://creativecommons.org/licenses/by-nc/4.0/" target="_blank">CC BY-NC 4.0</a></span><span class="icp-splitter">&nbsp;|&nbsp;</span><br class="icp-br"/>
                <span class="icp"><a href="http://beian.miit.gov.cn">苏ICP备2021012540号</a></span></div>
    </div>
</footer></div><a href="#" class="dynamic-to-top" id="dynamic-to-top" data-scroll>
            <span>&nbsp;</span>
        </a><script src="/js/lib/jquery/jquery.slim.min.js"></script><script src="/js/lib/lazysizes/lazysizes.min.js"></script><script src="/js/lib/smooth-scroll/smooth-scroll.polyfills.min.js"></script><script>window.scroll = new SmoothScroll('[data-scroll]', {speed: 300, speedAsDuration: true});</script><link rel="stylesheet" href="/css/lib/katex/katex.min.css"><script src="/js/lib/katex/katex.min.js"></script><script defer src="/js/lib/katex/auto-render.min.js"></script><link rel="stylesheet" href="/css/lib/katex/copy-tex.min.css"><script defer src="/js/lib/katex/copy-tex.min.js"></script><script defer src="/js/lib/katex/mhchem.min.js"></script><script>
        document.addEventListener("DOMContentLoaded", function () {
            renderMathInElement(document.body, {
                delimiters: [
                    { left: "$$", right: "$$", display: true },
                    { left: "\\(", right: "\\)", display: false },
                    { left: "\\[", right: "\\]", display: true },{ left: "$", right: "$", display: false },]
            });
        });
    </script>
    <script src="https://eqcn.ajz.miesnfu.com/wp-content/plugins/wp-3d-pony/live2dw/lib/L2Dwidget.min.js"></script>

    <script>
        var sUserAgent = navigator.userAgent.toLowerCase();
        if (/ipad|iphone|midp|rv:1.2.3.4|ucweb|android|windows ce|windows mobile/.test(sUserAgent)){
            
        }
        else{
            L2Dwidget.init({
                
                "model": {
                    
                    
                    
                    
                    
                    
                    
                    
                    
                    
                    
                    
                    
                    
                    
                    
                                
                    jsonPath: "/data/Shinomiya_Kaguya/model.model.json",
                    "scale": 1
                },
                
                "display": {
                    "position": "left",
                    "width": 150,
                    "height": 300,
                    "hOffset": 0,
                    "vOffset": 0
                },
                "mobile": {
                    "show": true,
                    "scale": 0.5
                },
                "react": {
                    "opacityDefault": 1,
                    "opacityOnHover": 0.2
                }
            });
                function changebottom() {
                            var canvas_temp = document.getElementById("live2dcanvas");
            canvas_temp.style="position: fixed; opacity: 1; left: 0px; bottom: -100px; z-index: 99999; pointer-events: none;";
                }

            window.onload=changebottom;
        }


    </script><script src="/js/blog.min.js"></script>
</body>
</html>